STM: event system typename wf

ABS: EventsWithOrder

STM: EOrder wf

ABS: EventsWithState

STM: E-State wf

STM: EState-subtype-EOrder

ABS: EventsWithKinds

STM: EKind wf

ABS: EventsWithValues

STM: EVal wf

ABS: ESMachineAxiom(E;T;V;M;loc;knd;val;when;after;sndr;Trans;Send;Choose)

STM: ESMachineAxiom wf

ABS: e = e'

STM: es-eq-E wf

STM: assert-es-eq-E

STM: assert-es-eq-E-2

STM: decidable es-E-equal

STM: test-eq-E-update

ABS: es-LnkTag-deq

STM: es-LnkTag-deq wf

ABS: case(kind(e))act(a) => f(a)rcv(l,tg) => g(l;tg)

STM: es-kindcase wf

ABS: msgtype(m)

STM: es-msgtype wf

STM: es-valtype-kindtype

ABS: state@i\\x

STM: es-state-without wf

STM: es-state-eta

STM: event system-level-subtype

ABS: mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v)

STM: mk-eval wf

ABS: AtomFreeDecls(X)

ABS: state when e\\x

STM: es-state-when-without wf

ABS: state after e\\x

STM: es-state-after-without wf

ABS: e c e'

STM: es-causle wf

STM: es-locl-trans

STM: es-locl-trichotomy

STM: es-le-trans

STM: es-locl transitivity

STM: es-locl transitivity1

STM: es-locl transitivity2

STM: es-le transitivity

STM: es-le weakening

STM: es-le weakening eq

STM: es-locl-trans-test

STM: es-locl-irreflex-test

STM: es-le-trans2

STM: es-le-trans3

STM: es-index-zero

STM: es-causle-trans

STM: es-causl-trans3

STM: es-causle transitivity

STM: es-causl transitivity

STM: es-causl transitivity1

STM: es-causl transitivity2

STM: es-causle weakening

STM: es-causle weakening eq

STM: es-causle weakening locl

STM: es-causl weakening

STM: es-causl-trans-test

STM: es-le-causle

STM: es-locl-total

STM: es-locl-total2

STM: same-loc-total

STM: same-loc-total2

STM: es-le-total

STM: es-locl-swellfnd

STM: es-causl-wellfnd

STM: es-causl-swellfnd

STM: es-le-not-locl

STM: es-causal-antireflexive

STM: es-causl irreflexivity

STM: es-causal-antisymmetric

STM: es-causl-locl

STM: es-causle-le

STM: es-pred-locl

STM: es-le-self

STM: es-pred-le

STM: es-pred-causl

STM: es-sender-causl

STM: es-sender-causle

STM: causl-trans-test2

STM: es-causle-retraction

ABS: f**(e)

STM: es-fix wf

STM: es-fix-cases

STM: es-time-sender

STM: es-first-implies

STM: es-loc-rcv

STM: es-isrcv-loc

STM: es-hasloc

STM: es-loc-sender

STM: same-sender-index

STM: es-le-iff

STM: es-first-le

STM: es-le-antisymmetric

STM: es-le antisymmetry

STM: es-first-unique

STM: es-causl-iff

STM: implies-es-pred

STM: es-le-pred

STM: implies-es-pred2

STM: es-pred-one-one

STM: decidable es-locl

STM: es-next

ABS: e <loc e'

STM: es-bless wf

STM: assert-es-bless

STM: decidable es-le

ABS: es-ble{i:l}(es;e;e')

STM: es-ble wf

STM: assert-es-ble

STM: decidable es-causl

STM: decidable es-causle

STM: decidable existse-causl

STM: decidable existse-causle

STM: decidable alle-causl

STM: decidable alle-causle

STM: decidable rel plus-causl

STM: decidable rel star-causl

STM: causal-sort

STM: es-sends-bound

STM: decidable existse-rcv

STM: es-minimal-event

ABS: es-bc{i:l}(es;e;e')

STM: es-bc wf

STM: assert-es-bc

ABS: e=k(v).P(e;v)

ABS: e:rvc(l,tg,v).P(e;v)

ABS: mval(m)

STM: es-mval wf

STM: es-mval-valtype

STM: es-msg-rcvd

ABS: before(e)

STM: es-before wf

STM: es-before wf2

STM: member-es-before

STM: l before-es-before

STM: l before-es-before-iff

ABS: es-le-before(es;e)

STM: es-le-before wf

STM: member-es-le-before

STM: es-causle-list

ABS: es-init(es;e)

STM: es-init wf

STM: es-init-le

STM: es-first-init

STM: es-init-identity

STM: es-init-elim

STM: es-init-elim2

STM: es-init-eq

STM: es-loc-init

ABS: [e, e']

STM: es-interval wf

STM: member-es-interval

STM: l before-es-interval

STM: hd-es-interval

STM: es-interval-non-zero

STM: es-interval-nil

STM: es-interval-is-nil

STM: es-interval-last

STM: es-interval-less

STM: es-interval-less-sq

STM: es-interval-eq

STM: es-interval-eq2

STM: es-interval-length-one-one

STM: es-interval-one-one

STM: es-interval-iseg

STM: es-interval-partition

STM: es-interval-select

STM: es-interval wf2

STM: es-le-before-partition

STM: es-le-before-partition2

ABS: haslnk(l;e)

STM: es-haslnk wf

STM: assert-es-haslnk

ABS: rcvs(l;before(e'))

STM: es-rcvs wf

STM: member-es-rcvs

ABS: snds(l;before(e))

STM: es-snds wf

STM: member-es-snds

ABS: snds(l, before(e,n))

STM: es-snds-index wf

STM: member-es-snds-index

STM: firstn-before

STM: es-before-decomp

STM: last-es-snds-index

ABS: emsg(e)

STM: es-msg wf

STM: es-msg wf2

STM: es-msg-member-sends

ABS: msgs(l;before(e'))

STM: es-msgs wf

STM: haslink wf2

STM: member-es-msgs

STM: es-fifo-nil

STM: es-fifo

STM: es-after-pred

STM: es-after-pred2

STM: decl-state-exists

STM: decl-state-subtype

ABS: @i always.P(x)

STM: alle-at1 wf

ABS: @i always.P(x1;x2)

STM: alle-at2 wf

STM: alle-at-iff

STM: alle-at-not-first

STM: es-invariant1

STM: es-invariant2

STM: es-constant1

ABS: e@i.P(e)

STM: existse-at wf

STM: change-lemma

STM: change-lemma2

STM: es-first-exists

STM: change-since-init

ABS: ee'.P(e)

STM: existse-le wf

ABS: e<e'.P(e)

STM: existse-before wf

STM: existse-before-iff

STM: decidable existse-before

STM: existse-le-iff

STM: decidable existse-le

ABS: e'e.P(e')

STM: alle-ge wf

ABS: e<e'.P(e)

STM: alle-lt wf

STM: alle-lt-iff

STM: decidable alle-lt

ABS: ee'.P(e)

STM: alle-le wf

STM: alle-le-iff

STM: decidable alle-le

ABS: e[e1,e2).P(e)

STM: alle-between1 wf

STM: alle-between1-trivial

STM: alle-between1-true

STM: alle-between1-false

STM: alle-between1 functionality wrt iff

STM: decidable alle-between1

ABS: e[e1,e2).P(e)

STM: existse-between1 wf

STM: existse-between1-true

STM: existse-between1-false

STM: existse-between1 functionality wrt iff

STM: decidable existse-between1

ABS: e[e1,e2].P(e)

STM: alle-between2 wf

STM: alle-between2-true

STM: alle-between2-false

STM: alle-between2 functionality wrt iff

STM: decidable alle-between2

ABS: e[e1,e2].P(e)

STM: existse-between2 wf

STM: existse-between2-false

STM: existse-between2-true

STM: existse-between2 functionality wrt iff

STM: decidable existse-between2

ABS: e(e1,e2].P(e)

STM: existse-between3 wf

STM: existse-between3-false

STM: existse-between3-true

STM: existse-between3 functionality wrt iff

STM: decidable existse-between3

ABS: e(e1,e2].P(e)

STM: alle-between3 wf

STM: alle-between3-false

STM: es-subinterval

STM: last-change

ABS: e is first@ i s.t.  e.P(e)

STM: es-first-at wf

STM: es-first-before

STM: es-first-before2

ABS: es-first-at-since(es;i;e;e.R(e);e.P(e))

STM: es-first-at-since wf

STM: previous-event-exists

STM: es-first-at-since-iff

ABS: es-first-at-since'(es;i;e;e.R(e);e.P(e))

STM: es-first-at-since' wf

ABS: e=rcv(l,tg).P(e)

STM: alle-rcv wf

ABS: e=rcv(l,tg).P(e)

STM: existse-rcv wf

STM: es-bound-list

STM: es-bound-list2

STM: es-machine-axiom

ABS: e receives || a

STM: es-rcv-atom wf

ABS: e sends || a

STM: es-send-atom wf

ABS: e sends to i || a 

STM: es-send-atom-to wf

ABS: e leaks x to e'

ABS: e copies x

STM: state-after-pred

STM: implies-es-atom-axiom

ABS: i || a

STM: es-atom wf

STM: es-copies wf

STM: es-leaks wf

STM: es-atom-axiom

STM: es-atom-lemma1

STM: es-atom-lemma2

ABS: @i discrete ds

STM: es-dds wf

STM: es-dds-single

ABS: discrete state@i

STM: es-dstate wf

STM: es-state-dstate-subtype

STM: es-dstate-subtype

ABS: (discrete state when e)

STM: es-dstate-when wf

STM: es-state-when-dstate-when

ABS: (discrete state after e)

STM: es-dstate-after wf

STM: es-state-after-dstate-after

STM: dstate-after-pred

STM: alle-between1-after

STM: alle-between1-after-1

ABS: @i stable state.P(state)  

STM: es-stable wf

STM: stable-implies

STM: stable-implies2

STM: stable-implies3

STM: stable-implies4

ABS: @i Precondition for a(Outcome(p)) P discrete state(ds)

STM: discrete-pre-p wf

STM: last-event

ABS: last-solution(es;P;d)

STM: last-solution wf

STM: last-transition

STM: last-decidable

STM: last-state-change

STM: last-state-change2

STM: last-state-change3

ABS: @i only L affect x:T

STM: es-frame wf

STM: frame-p-es-frame

STM: es-stable-1

STM: es-stable-2

STM: es-stable-3

STM: es-constant-1

ABS: es-responsive(es;l1;tg1;l2;tg2)

STM: es-responsive wf

STM: es-responsive-bijection

ABS: only k(v):B sends [tg,f(s;v)] : T on l

STM: es-only-sender wf

ABS: @i x has type T

STM: vartype-es-type

STM: vartype-es-state-sub

STM: es-state-subtype

STM: es-state-subtype-iff

STM: es-state-subtype2

STM: state-after-pred-ds

STM: es-invariant

STM: state-when-first

STM: es-when-first

STM: es-when-init

STM: es-discrete-when-first

STM: es-when-first-discrete

STM: dds-state-after-elapsed

STM: dds-init-elapsed

STM: init-p-implies

ABS: usends1-p(es;ds;k;T;l;tg;B;f)

STM: usends1-p wf

STM: usends1-function

ABS: sends1-p(es;x;A;k;B;l;tg;T;f)

STM: sends1-p wf

STM: sends-p-implies-sends1-p

ABS:  k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v)

STM: conditional-send1-p wf

STM: sends1-p-implies-conditional-send1-p

STM: conditional-send1-function

ABS: k(v:B) sends on l [tg:T, f <state, v>]?[]

STM: conditional-send-p wf

STM: sends-p-implies-conditional-send-p

ABS: pre-init1-p(es;i;x;X;x0;a;p;P)

STM: pre-init1-p wf

ABS: weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)

STM: weak-precond-send-p wf

ABS: discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)

STM: discrete-weak-precond-send-p wf

STM: wps-implies-discrete-wps

ABS: weak-send-do-apply(es;T;l;tg;a;ds;f)

STM: weak-send-do-apply wf

ABS: @i locl(a) occurs once

STM: once-p wf

ABS: locl(a) sends [tg,f{AT}(x)] on link l once

STM: send-once-p wf

ABS: recognizer-p(es;T;A;P;k;i;r;x)

STM: recognizer-p wf

ABS: recognizer(es;i;ds;x;k;T;test)

STM: recognizer wf

ABS: @i k(v:T) triggers local action a when P (x:A) v

STM: trigger1-p wf

STM: es-interval-induction

STM: es-interval-induction2

ABS: PossibleEvent(poss)

STM: possible-event wf

ABS: pe-es(e)

STM: pe-es wf

ABS: pe-e(p)

STM: pe-e wf

ABS: pe-state(p)

STM: pe-state wf

ABS: pe-loc(p)

STM: pe-loc wf

ABS: K(P)@e

STM: es-knows wf

STM: es-knows-true

STM: es-knows-knows

STM: es-knows-not

STM: es-knows-trans

STM: es-knows-valid

ABS: e1  e2

STM: poss-le wf

STM: es-knows-stable

ABS: e:s.P(s)@j 

STM: es-simul wf

ABS: es-decls(es;i;ds;da)

STM: es-decls wf

STM: es-decls-iff

STM: es-decls-join-single

ABS: with decls ds dasends on l from e include f(e) and only these for tags in tgs

STM: es-sends-iff wf

ABS: state dsk:A sends [tg, e.f(e):B] on l

STM: es-kind-sends-iff wf

STM: es-sends-iff functionality

ABS: es-update-iff(es;i;x;ds;e.P(e);s.f(s))

STM: es-update-iff wf

ABS: (e sends on l with tag tg)

STM: es-sends-on wf

ABS: es-first-from(es;e;l;tg)

STM: es-first-from wf

STM: es-kind-first-from

STM: es-loc-first-from

ABS: loc-on-path(es;i;L)

STM: loc-on-path wf

STM: loc-on-path-append

STM: loc-on-path-cons

STM: loc-on-path-nil

STM: loc-on-path-singleton

STM: es-sender-first-from

STM: es-first-from-is-first

ABS: es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))

STM: es-sends-iff2 wf

STM: es-sends-iff2 functionality

ABS: event-info(ds;da)

STM: event-info wf

ABS: es-info(es;e)

STM: es-info wf

ABS: es-hist{i:l}(es;e1;e2)

STM: es-hist wf

STM: member-es-hist

STM: null-es-hist

STM: es-hist-iseg

STM: es-hist-partition

STM: es-hist-last

STM: last-es-hist

STM: es-hist-is-append

STM: es-hist-is-concat

STM: iseg-es-hist

STM: es-hist-one-one

ABS: es-trans-state-from{i:l}(es;ks;g;z;e1;e2)

STM: es-trans-state-from wf

ABS: e2 = first e  e1.P(e)

STM: es-first-since wf

STM: es-first-since functionality wrt iff

STM: alle-between1-not-first-since

STM: alle-between2-not-first-since

STM: es-increasing-sequence

STM: es-increasing-sequence2

ABS: [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)

STM: es-pstar-q wf

STM: es-pstar-q-trivial

STM: es-pstar-q-le

STM: es-pstar-q functionality wrt implies

STM: es-pstar-q functionality wrt rev implies

STM: es-pstar-q functionality wrt iff

STM: es-pstar-q-partition

ABS: [e1,e2]~([a,b].p(a;b))+

STM: es-pplus wf

STM: es-pplus functionality wrt implies

STM: es-pplus functionality wrt rev implies

STM: es-pplus functionality wrt iff

STM: es-pplus-trivial

STM: es-pplus-le

STM: es-pplus-alle-between2

STM: es-pplus-partition

STM: es-pplus-first-since

STM: es-pplus-first-since-exit

ABS: data(T)

STM: data wf

ABS: secret-table(T)

STM: secret-table wf

ABS: ||tab|| 

STM: st-length wf

ABS: ptr(tab)

STM: st-ptr wf

ABS: st-atom(tab;n)

STM: st-atom wf

ABS: atoms-distinct(tab)

STM: st-atoms-distinct wf

ABS: next(tab)

STM: st-next wf

ABS: key(tab;n)

STM: st-key wf

ABS: data(tab;n)

STM: st-data wf

STM: st-ptr-wf2

ABS: st-lookup(tab;x)

STM: st-lookup wf

STM: st-lookup-property

STM: st-lookup-outl

STM: st-lookup-distinct

ABS: st-key-match(tab;k1;k2)

STM: st-key-match wf

ABS: decrypt(tab;kval)

STM: st-decrypt wf

ABS: encrypt(tab;keyv)

STM: st-encrypt wf

STM: st-length-encrypt

STM: st-atom-encrypt

ABS: ?[x]

STM: cond-to-list wf

ABS: es-secret-server

STM: es-secret-server wf

STM: ss-ptr-non-decreasing

STM: ss-table-length

STM: ss-atom-constant

STM: ss-atoms-distinct

STM: ss-encrypt-unique

ABS: es-seq(es;S)

STM: es-seq wf

STM: send-minimal-lemma

ABS: @e(xv)

STM: es-change-to wf

STM: change-to-lemma

STM: change-to-lemma2

ABS: change-to(x;e)

STM: change-to wf

ABS: x changed before e

STM: changed wf

ABS: (last change to x before e)

STM: last-change wf

STM: last-change-property

STM: last-change-after-property

STM: change-to-last-change

STM: after-last-change

STM: loc-last-change

STM: assert-changed

STM: not-changed

STM: has-changed

STM: last-change-pred

STM: init-changed

STM: init-not-changed

STM: last-change-equal

STM: last-change-equal2

STM: es-le-last-change

ABS: lastchange(x;e)

STM: es-lc wf

STM: es-lc-init-p

STM: es-lc-after

STM: es-loc-lc

STM: es-lc-le

STM: es-after-lc-before

STM: es-lc-no-change

STM: es-lc-no-change2

STM: es-lc-cases

STM: es-lc-cases2

STM: es-lc-bool

STM: es-lc-btrue

STM: es-lc-unique

STM: es-lc-equal

STM: once-lemma

STM: const-lemma1

STM: const-lemma

STM: next-state-relation

STM: next-var-value

ABS: next event in [e;bound] after which x = v

STM: es-next-assign wf

STM: es-next-assign-property

STM: es-next-assign-unique

ABS: next event in [e,bound] after which x = b

STM: es-next-bool-assign wf

STM: es-next-bool-assign-property

ABS: (x unchanged-for t @ e)

STM: unchanged-for wf

STM: es-causle-time

STM: es-causl-fifo

STM: unchanged-for-change-to

ABS: val(e)  val(e')

STM: es-same-val wf

ABS: AbsInterface(A)

STM: es-interface wf

STM: es-interface-subtype rel

ABS: f'Ia

STM: es-interface-image wf

STM: p-first wf-interface

ABS: es-in-port(es;l;tg)

STM: es-in-port wf

ABS: es-trigger(es;i;knd;ds;f)

STM: es-trigger wf

ABS: es-triggers(es;i;ds;conds)

STM: es-triggers wf

ABS: es-in-port-conds(A;l;tg)

STM: es-in-port-conds wf

STM: es-in-port-triggers

ABS: es-triggers-params-consistent(es;A;i;ds;conds)

STM: es-triggers-params-consistent wf

STM: es-triggers-params-join

STM: es-triggers-params-list-join

STM: functions-decl-state

STM: es-interface-conditional

ABS: es-interface-left(X)

STM: es-interface-left wf

ABS: es-interface-right(X)

STM: es-interface-right wf

ABS: e  X

STM: es-is-interface wf

ABS: es-interface-empty(es;I)

STM: es-interface-empty wf

ABS: Empty

STM: es-empty-interface wf

ABS: isempty{isempty_compseq_tag_def:ObjectId}(e)

STM: es-empty-interface-property

STM: es-trigger-not-loc

STM: es-trigger-loc

STM: es-triggers-not-loc

STM: es-triggers-loc

ABS: {I}

STM: es-interface-predicate wf

STM: es-interface-conditional-domain

STM: es-interface-conditional-domain-iff

STM: es-interface-conditional-predicate-equivalent

STM: es-interface-conditional-domain-member

ABS: E(X)

STM: es-E-interface wf

STM: decidable equal es-E-interface

ABS: es-interface-sublist(X;z)

STM: es-interface-sublist wf

STM: es-E-interface-subtype

STM: es-E-interface-subtype rel

STM: es-E-interface-strong-subtype

STM: es-E-interfaces-strong-subtype

STM: es-E-interface functionality

STM: es-E-interface-conditional

STM: es-E-interface-conditional2

STM: es-E-interface-conditional-subtype1

STM: es-E-interface-conditional-subtype2

STM: es-causle-interface-retraction

STM: es-fix wf2

STM: es-fix property

STM: es-fix-equal

STM: es-fix-step

STM: es-fix-connected

STM: es-fix-sqequal

STM: es-fix-equal-E-interface

STM: fun-connected-causle

STM: loc-on-path-decomp

STM: es-fix-causle

STM: es-fix-causl

STM: es-is-interface-image

STM: es-E-interface-image

STM: es-E-interface-predicate

ABS: es E interface predicate compseq tag def

ABS: X(e)

STM: es-interface-val wf

STM: es-interface-val wf2

ABS: X(L)

STM: es-interface-vals wf

STM: es-interface-vals-append

STM: es-interface-image-val

STM: es-interface-extensionality

STM: es-interface-image-trivial

STM: es-interface-val-conditional

STM: es-interface-val-disjoint

ABS: (I|p)

STM: es-interface-restrict wf

ABS: (I|p)

STM: es-interface-co-restrict wf

STM: es-is-interface-restrict

STM: es-is-interface-restrict-guard

STM: es-is-interface-restrict2

STM: es-is-interface-co-restrict

STM: es-interface-val-restrict

STM: es-interface-val-restrict-sq

STM: es-interface-val-co-restrict

STM: es-interface-restrict-trivial

STM: es-interface-restrict-idempotent

STM: es-E-interface-restrict

STM: es-E-interface-co-restrict

ABS: X  Y = 0

STM: es-interface-disjoint wf

STM: es-interface-restrict-disjoint

STM: es-interface-restrict-conditional

ABS: X|a.P(a)

STM: es-interface-filter wf

STM: es-is-interface-filter

STM: es-interface-filter-val

STM: es-is-interface-in-port

STM: es-is-interface-trigger

STM: es-is-interface-triggers

STM: es-is-interface-triggers2

STM: es-triggers-conditional

STM: es-is-interface-p-first

STM: es-E-interface-p-first

STM: es-triggers-p-first

STM: es-in-port-val

STM: es-trigger-val

STM: es-triggers-val

STM: es-in-port-receives

ABS: X is local

STM: es-interface-local wf

ABS: X is finite

STM: es-interface-finite wf

STM: es-interface-finite-implies

ABS: es-interface-history(es;X;e)

STM: es-interface-history wf

STM: es-interface-history-first

STM: es-interface-history-pred

STM: es-interface-history-iseg

STM: member-es-interface-history

STM: nonempty-es-interface-history

STM: es-interface-from-decidable

ABS: es-p-local-pred(es;P)

STM: es-p-local-pred wf

ABS: es-p-le-pred(es;P)

STM: es-p-le-pred wf

STM: decidable es-p-local-pred

STM: decidable es-p-le-pred

STM: decidable exists-es-p-local-pred

STM: decidable exists-es-p-le-pred

STM: es-interface-local-pred

STM: es-interface-le-pred

STM: es-interface-local-pred-bool

STM: es-interface-le-pred-bool

ABS: last(P)

STM: es-local-pred wf

STM: es-local-pred-property

ABS: es-local-le-pred{i:l}(es;P)

STM: es-local-le-pred wf

STM: es-local-le-pred-property

ABS: prior(X)

STM: es-prior-interface wf

ABS: le(X)

STM: es-le-interface wf

STM: es-is-prior-interface

STM: es-is-prior-interface-pred

STM: es-is-le-interface

STM: es-is-le-interface-iff

STM: es-prior-interface-val

STM: es-le-interface-val

STM: es-le-interface-val-cases

STM: es-prior-interface-val-pred

STM: es-prior-interface-locl

STM: es-prior-interface-causl

STM: es-le-prior-interface-val

STM: es-prior-interface-val-locl

STM: es-le-interface-le

STM: es-le-interface-causle

STM: es-interface-history-prior

ABS: prior-state(f;base;X;e)

STM: es-local-prior-state wf

ABS: local-state(f;base;X;e)

STM: es-interface-local-state wf

STM: es-interface-local-state-prior

STM: es-interface-local-state-cases

ABS: es-prior-interface-vals(es;X;e)

STM: es-prior-interface-vals wf

STM: es-prior-interface-vals-property

STM: local-prior-state-accumulate

ABS: e(X)

STM: es-interface-sum wf

STM: es-interface-sum-cases

STM: es-interface-sum-le-interface

ABS: prior-f-fixedpoints(e)

STM: es-prior-fixedpoints wf

STM: es-prior-fixedpoints-fix

STM: member-es-fix-prior-fixedpoints

STM: es-fix-last-prior-fixedpoints

STM: es-prior-fixedpoints-non-null

STM: es-prior-fixedpoints-causle

STM: es-prior-fixedpoints-iseg

STM: es-prior-fixedpoints-no repeats

STM: es-prior-fixedpoints-fixed

STM: es-prior-fixedpoints-unequal

ABS: ComponentSpec(A;B)

STM: es-component wf

ABS: es-decl(es;ds;da)

STM: es-decl wf

ABS: [P? f : g]

STM: conditional wf

STM: conditional wf2

STM: conditional-idempotent

STM: conditional-ifthenelse

STM: conditional-apply

STM: conditional wf-interface

STM: conditional wf-interface2

ABS: Q ==f== P

STM: weak-antecedent-function wf

STM: weak-antecedent-function-property

STM: weak-antecedent-function functionality wrt pred equiv

STM: weak-antecedent-functions-compose

STM: weak-antecedent-conditional

ABS: Q = f== P

STM: weak-antecedent-surjection wf

STM: weak-antecedent-surjection-property

STM: weak-antecedent-surjection functionality wrt pred equiv

STM: weak-antecedent-surjections-compose

STM: weak-antecedent-surjection-conditional

STM: weak-antecedent-surjection-conditional2

ABS: f is Q-R-pre-preserving on P

STM: Q-R-pre-preserving wf

STM: Q-R-pre-preserving functionality wrt implies

STM: Q-R-pre-preserving-rewrite-test

STM: Q-R-pre-preserving-compose

STM: Q-R-pre-preserving-1-1

STM: Q-R-pre-preserving-conditional

STM: sender-le-pre-preserving

ABS: f is R-pre-preserving on P

STM: rel-pre-preserving wf

STM: rel-pre-preserving-compose

ABS: f is locl-pre-preserving on P

STM: locl-pre-preserving wf

STM: locl-pre-preserving-compose

STM: locl-pre-preserving-1-1

ABS: g glues Ia:Qa f Ib:Rb

STM: Q-R-glues wf

STM: Q-R-glues-property

STM: Q-R-glues functionality

STM: Q-R-glues-empty

STM: Q-Q-glues-to-self-image

STM: Q-Q-glues-to-self

STM: inject-composes

STM: Q-R-glues-composes

STM: Q-R-glues-composes2

STM: Q-R-glues-conditional

STM: Q-R-glues-conditional2

STM: Q-R-glues-split

STM: Q-R-glues-trivial-restrict

STM: Q-R-glues-trivial-split

ABS: Ia:Qa f  Ib:Rb

STM: Q-R-glued wf

STM: Q-R-glued-empty

STM: Q-Q-glued-self-image

STM: Q-Q-glued-to-self

STM: Q-R-glued-composes

STM: Q-R-glued-conditional

STM: Q-R-glued-first

ABS: g glues Ia f Ib

STM: glues wf

STM: glues-property

ABS: glued(es;B;f;Ia;Ib)

STM: glued wf

STM: glued-Q-R-glued

STM: glued-to-self

STM: glue-composes

STM: glued-composes

STM: glued-composes-simple

STM: glued-first

STM: sender-glues-trigger

STM: sender-glues-triggers

STM: sender-glues-triggers2

STM: sender-frame-glues-triggers

ABS: sender-glues-triggers-p(es;A;l;tg;ds;conds)

STM: sender-glues-triggers-p wf

ABS: triggers-glued-p(es;A;l;tg;ds;conds)

STM: triggers-glued-p wf

STM: sender-glues-implies-triggers-glued

STM: causal-p-predecessor

ABS: retrace(es;Q;X)

STM: retrace wf

ABS: retracer(p)

STM: retracer wf

ABS: state-machine-spec{i:l}(es;C;R;F;I;O)

STM: state-machine-spec wf

DIR: abstract chain replication

DIR: chain replication